Inference at * 1 
Iof proof for Lemma p-fun-exp-injection:

.....basecase..... NILNIL

1. A : Type
2. f : A(A + Top)
3. p-inject(A;A;f)
  p-inject(A;A;f^0) 

latex

 by (RepUR ``p-inject p-fun-exp p-id can-apply do-apply`` ( 0)) 
CollapseTHEN (Auto) 

latex

C.

Definitions

f^n, p-inject(A;B;f), can-apply(f;x), p-id(), do-apply(f;x), b, x:A. B(x), True, P  Q, s = t